Papers with Automated Theorem Proving
Learn from Failure: Fine-tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving (2024.acl-long)
Copied to clipboard
Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, Jingbo Shang
| Challenge: | Recent advances in Automated Theorem Proving have shown the effectiveness of leveraging a (large) language model that generates tactics (i.e. proof steps) to search through proof states. |
| Approach: | They propose to use a large language model that generates tactics to search through proof states. |
| Outcome: | The proposed model solves more unseen theorems with lower trial searches than the current model, which only learns from failed attempts. |
Neural Unification for Logic Reasoning over Natural Language (2021.findings-emnlp)
Copied to clipboard
| Challenge: | Automated Theorem Proving (ATP) is a computer program that can show that conjectures are logical consequences of a set of axioms. |
| Approach: | They propose a transformer-based architecture for deriving conjectures given axioms . they propose 'neural unifier' and relative training procedure to train the model . |
| Outcome: | The proposed architectures are able to answer queries with deep queries with a relatively low training time. |
QDTSynth: Quality-Driven Formal Theorem Synthesis for Enhancing Proving Performance of LLMs (2025.acl-long)
Copied to clipboard
| Challenge: | Existing formal languages such as Lean, Coq and Metamath are proving to be useful in formal theorem proving . however, there is a scarcity of high-quality supervised fine-tuning data for formal proofs . |
| Approach: | They propose a Q**uality-**D**riven **T**heorem **S**ynthesis method in Lean4 . they propose diversity screening and the self-assessment method to select theoremas that exhibit diversity and high quality from the initial synthetic statements. |
| Outcome: | The proposed method significantly improves performance of open-source LLMs in theorem proving tasks. |
EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving (2026.acl-long)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) have recently advanced the field of Automated Theorem Proving (ATP) Existing cost analyses regulate only the number of sampling passes, ignoring the substantial disparities in sampling costs. |
| Approach: | They propose to integrate two complementary methods into a unified EconRL pipeline to increase pass rates under constrained sampling passes. |
| Outcome: | The proposed method reduces token usage and sample passes while maintaining the original performance. |